\begin{tabbing}
fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$), ${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex](es{-}loc(${\it es}$; $e$) = es{-}loc(${\it es}$; ${\it e'}$) $\in$ Id) $\Rightarrow$ es{-}le(${\it es}$;$f$($e$);$f$(${\it e'}$)) $\Rightarrow$ es{-}le(${\it es}$;$e$;${\it e'}$)
\-
\end{tabbing}